a:Id, T, A:Type, x:Id, P:(ATProp).
T
 A
 AtomFree(Type;A)
 AtomFree(Type;T)
 (a:A. Dec(v:T. P(a,v)))
 Feasible(ma-single-pre1(x;A;a;T;x,v.P(x,v))) 

latex

Definitions	IdDeq, x:A. B(x), P  Q, xdom(f). v=f(x)   P(x;v), State(ds), Void, x:A. B(x), Top, f(x)?z, x:AB(x), x.A(x), x. t(x), f(a), x(s1,s2), x:AB(x), x:A. B(x), Dec(P), x,y. t(x;y), ma-single-pre1(x;A;a;T;y,v.P(y;v)), Prop, AtomFree(T;x), Feasible(M), x : v, Type, Id, a:A fp B(a), t  T
Lemmas	decidable wf, atom-free wf, fpf-single wf, ma-single-pre-feasible, fpf-cap-single1, fpf-cap wf, top wf, ma-state wf, non-void-decl-single, atom-free-decl-single, Id wf, id-deq wf